#ifndef FORMULA_HH
# define FORMULA_HH
#include "cuddObj.hh"
#include <map>
#include <vector>

using namespace std;

class Formula {
  /* 0: term, 1=AND, 2=OR, 3=NOT, 4=IMPLIES,
     10=AG, 11=EG, 12=AX, 13=EX, 14=AF, 15=EF, 16=AU, 17=EU,
     30=K ("standard" knowledge),
     31=KPR (perfect recall),
     32=KB (bounded recall)
  */
  unsigned short int op; // type of node
  string name; // name of the variable if it's a term
  unsigned short int depth; // depth of bounded recall
  unsigned int model_depth; // the max computation depth (used by
			   // perfect recall, computed by
			   // compute_reachable_states
  vector<BDD*>* EC; // Equivalence classes for epistemic
		    // relation. Just a single one here, it should be
		    // a map agent name -> EC (or something like that)

  Formula *left;
  Formula *right;

public:
  Formula(string name); // term
  Formula(unsigned short int o, Formula *f1); // sigle operand formula
  Formula(unsigned short int o, Formula *f1, Formula *f2); // two operands formula

  // Setters
  void set_depth(unsigned short int d); // set depth
  void set_name(string name); // set the name
  void set_model_depth(unsigned int d); // set model depth
  void set_EC(vector<BDD*> *EC); // set equivalence classes (see
				 // above)

  // Getters
  unsigned short int get_op();
  string get_name();
  unsigned short int get_depth();
  unsigned int get_model_depth();
  vector<BDD *>* get_EC();
  Formula* get_left();
  Formula* get_right();
  
  // Everything else
  string to_string(); 
  BDD* check_formula(BDDvector *v, BDDvector *pv, BDD *Rt, 
		     BDD *Ri, Cudd *bddmgr, map<string, BDD*> *evaluation, BDD *reach );
};


#endif // FORMULA_HH
